the_es:ES, m:Msg. mlnk(m)  IdLnk 

latex

Definitions	t  T, x:A. B(x), Msg(M), mlnk(m), Msg, ES
Lemmas	event system wf, mlnk wf, Msg wf